M:MsgA, k:Knd, s:M.state, v:M.da(k). ma-has-sends(M;k)  M.sends(k,s,v) = nil  M.Msg List 

latex

Definitions

b, ma-has-sends(M;k), M.sends(k,s,v), Valtype(da;k), M.state, M.da(a), M.Msg, MsgA, t  T, Knd, x:A. B(x), A, P  Q, Msg(da), xL. P(x), IdLnk, x. t(x), 1of(t), KindDeq, eqof(d), State(ds), Top, f(x)?z, Id, rcv(l,tg), 2of(t), tagged-messages(l;s;v;L), , IdLnkDeq, product-deq(A;B;a;b), fpf-vals(eq;P;f), map(f;as), P  Q, P & Q, P  Q, {T}, SQType(T), Prop, mlnk(m), x(s1,s2), S  T, S  T, Msg(M), (x  l), x:A. B(x), let x = a in b(x), remove-repeats(eq;L), filter(P;l), False, a:A fp B(a), ij, ||as||, AB, , tl(l), i<j, b, ij, nth_tl(n;as), hd(l), l[i], i=j, NatDeq, atom-deq-aux, x=yAtom, AtomDeq, IdDeq, prod-deq(A;B;a;b), p  q, proddeq(a;b), sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), f(x), p  q, Y, reduce(f;k;as), deq-member(eq;x;L), x  dom(f), if b t else f fi

Lemmas

nil member, fpf wf, le wf, length wf1, non neg length, cons one one, IdLnk sq, remove-repeats property, assert-deq-member, not functionality wrt iff, filter is nil, remove-repeats wf, member map, l member wf, tagged-messages wf, deq property, Knd sq, concat-is-nil, map wf, ma-Msg wf, assert wf, fpf-vals wf, product-deq wf, idlnk-deq wf, Id wf, ma-state wf, top wf, fpf-cap wf, rcv wf, pi2 wf, eqof wf, Kind-deq wf, pi1 wf, IdLnk wf, not wf, ma-has-sends wf, ma-da wf, ma-st wf, Knd wf, msga wf